Static analysis involves analyzing a program without actually dynamically testing the program code through execution. Like dynamic testing, static analysis can discover errors in the program. Unlike dynamic testing, static analysis is neutral with respect to the distinction between typical scenarios and corner case scenarios. (Corner case scenarios are associating with atypical operating conditions). As a result, static analysis can often find corner case errors that are difficult to discover with dynamic testing. Also, unlike dynamic testing, static analysis can better guarantee that a program lacks errors of certain categories (in the case that the static analysis fails to find such errors in the program). Because of these features, developers and other individuals now routinely rely on static analysis tools to complement more traditional dynamic testing tools. Static analysis tools have proven especially useful in investigating safety-critical software, such as system software.
Some static analysis tools use a Counter-Example Guided Abstraction Refinement (CEGAR) loop to analyze an input program. In this technology, an abstraction component generates an abstraction of the input program with the intent of determining whether or not the program satisfies a property under investigation. A model checking component determines whether error states associated with the property are reachable. The model checking concludes that the program is free of defects (with respect to the property under investigation) if the error states are not reachable. On the other hand, if the model checker can reach an error state, it identifies an error trace which represents a sequence of program statements which lead to the error state. The trace can represent either a feasible trace (which represents an actual error in the program) or an infeasible trace (which does not represent an actual error). The CEGAR loop may generate infeasible traces because it is operating on a sometimes highly abstracted version of the input program that does not represent the full wealth of program states in that program.
The CEGAR loop next employs a validation component to determine whether the trace presents a feasible or infeasible trace. If the validation component concludes that the candidate trace is feasible, then the CEGAR loop has identified an actual error in the program. If the validation component concludes that the candidate trace is infeasible, then it next attempts to provide an explanation that accounts for why the program abstraction generated an inaccurate trace. In doing so, the validation component can identify one or more predicates. Predicates represent relations between variables, properties, etc.; the variables and properties, in turn, may pertain in various ways to the instrumented program being analyzed.
The abstraction component next generates a new abstraction of the input program on the basis of a current set of predicates which includes the newly discovered predicates. The model checking component then repeats its reachability analysis on the new abstraction generated by the abstraction component. The new abstraction will prevent the model checking component from reaching the error state along the same trace that it previously identified. However, the model checking component may still identify another trace that leads to an error state. In the manner described above, the CEGAR loop can repeat its validation, abstraction, and checking operations a plurality of times in order to reach a final conclusion as to whether or not the program satisfies the property under investigation (if such a final conclusion can be reached, which is not guaranteed).
CEGAR loop functionality has amply proven its usefulness in recent years. Representative tools that use CEGAR loop functionality go by the acronyms of Slam, Moped, Blast, F- Soft, Magic, and so on. For example, a first generation of the Slam product, provided by Microsoft Corporation of Redmond, Washington, is well-documented in the technical literature, e.g., as described in: Ball, et al., “The SLAM Project: Debugging System Software via Static Analysis,” in Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002, pp. 1-3; Ball, et al., “The SLAM Toolkit,” in Proceedings of the 13th International Conference on Computer Aided Verification, 2001, pp. 260-264; and Ball, et al., “Thorough Static Analysis of Device Drivers,” in Proceedings of the 2006 EuroSys Conference, 2006, pp. 73-85.
CEGAR loop functionality, while successful, is being asked to analyze programs and systems of increasing complexity and sophistication. There remains ample room for improving the efficiency and effectiveness of CEGAR loop functionality to keep pace with increasing demands placed on this functionality.